Nuprl Lemma : R-compat-Rplus2 0,22

ABC:Realizer. A || B  C  A || B & A || C 
latex


Definitionsx:AB(x), P  Q, A || B, P & Q, Prop, t  T, xt(x), Y, if b t else f fi, Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), false, true, P  Q, P  Q, Top, Realizer, Unit, x(s), left  right, , , @loc x initially v:T, @loc only events in L change x:T, only events in L send on lnk with tag, @loc effect knd(v:T)  x := f State(ds) v , sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc precondition for a(v:T):P State(ds) v, @lock writes only members of L, @lock sends only on links in L, @loc: only members of L read x
Lemmasunit wf, Id wf, Knd wf, IdLnk wf, fpf wf, decl-state wf, decl-type wf, R-compat wf, Rnone wf, es realizer wf, Rinit wf, Rframe wf, Rsframe wf, Reffect wf, Rsends wf, Rpre wf, Raframe wf, Rbframe wf, Rrframe wf, R-compat-Rplus-sq

origin